『On Universe in Type Theory』
1. どんなもの？
型理論における「宇宙（universe）」の概念について研究し、新たな拡張を提案する。特に、宇宙形成演算子（universe-forming operator）$ U(A,(x)B) や、それを含むスーパー宇宙（super universe）を導入し、型理論の証明論的強度を高める手法を探る。
2. 先行研究と比べてどこがすごい？
これまでの型理論では、宇宙は階層的に導入されるものの、トランスフィニットな（transfinite、超限階層の）構造は明確に定義されていなかった。
transfinite: 超限
本論文では、次のような新規性がある：
宇宙形成演算子 $ U(A,(x)B) の導入により、宇宙の階層構造を生成できる。
スーパー宇宙 $ (V,S) を定義し、宇宙のさらなる拡張を可能にした。
証明論的強度の評価を行い、従来の理論と比較して $ Γ_0, Φ_{ε0}(0), Φ_{Γ0}(0) などの強度を持つことを証明した。
3. 技術や手法のキモはどこ？
宇宙形成演算子$ U(A,(x)B) : 宇宙の階層構造を生成する演算子を定義し、それを用いたスーパー宇宙を構築。
スーパー宇宙$ (V, S) : 通常の宇宙に加えて、宇宙形成演算子に閉じたスーパー宇宙を導入。
証明論的強度: 既存の型理論と比較し、証明論的強度を評価し、強力な証明体系を構築。
4. どうやって有効だと検証した？
証明論的解析を通じて、宇宙の拡張が証明可能な命題の範囲を拡張することを示した。
具体的には、Rathjenによる証明論的強度の計算を用い、提案する拡張が$ Γ_0 や$ Φ_{ε0}(0) といった強度を持つことを確認。
型理論の整合性や、宇宙を含む理論がどのような数学的原理を表現できるかを分析。
5. 議論はある？
無限階層の宇宙の扱い: 宇宙をトランスフィニットに拡張する際の課題として、内部インデックスの必要性が指摘される。
反映原理の有用性: ある種の宇宙構造では、集合の同値性を反映させるべきかどうかが議論される。
非可述的（impredicative）型理論: 一部の拡張（例: Setzerのマーロー宇宙（Mahlo universe））では、非可述的な特徴が問題となる可能性がある。 6. 次に読むべき論文は？
P. Martin-Löf (1984). "Intuitionistic Type Theory" - 型理論の基礎的な定義と宇宙の概念に関する詳細な説明。
M. Rathjen (1997). "The strength of some universe constructions in Martin-Löf type theory" - 宇宙の証明論的強度に関する詳細な研究。
A. Setzer (1995). "A type theory for one Mahlo universe" - Mahlo universeの型理論への応用に関する研究。
U. Berger & H. Schwichtenberg (1995). "Program extraction from classical proofs" - 古典的証明からのプログラム抽出手法に関する研究。
メモ
$ T(\cdot) : デコード関数
$ U \ type \quad \frac{a \in U}{T(a) \ type}
$ U \ type \quad \frac{A \in U}{A \ type}
table:訳
universe 宇宙
super universe スーパー宇宙？、超宇宙？
propositions-as-types principle 命題＝型の原理
constructive type theory 構成的型理論 constructive set theory 構成的集合論
separation axiom 分離公理
proof-theoretic strength 証明論的強度
inductive definability 帰納的定義可能性？
large cardinal 大きな基数（大基数）
classical reasoning 古典的推論
logical framework 論理的枠組み
dependent function space 依存関数空間
Pi-type (Π-type) Π型(依存積型) Sigma-type (Σ-type) Σ型(依存和型) inductive set former 帰納的集合形成子
well-order type(W-types) 整列順序型
ordinal 順序数
Veblen function フェブレン関数
Howard ordinal ハワード順序数
impredicative theory 非可述的理論
strong subsystem 強い部分系
Kripke–Platek set theory クリプケ–プラテック集合論
second order arithmetic 二階算術
A-translation A-翻訳?
program extraction プログラム抽出
normalization 正規化
proof assistant 証明支援系
constructive justification 構成的正当化？
computation rule 計算規則
fixed point 不動点
ordinal analysis 順序数解析
strongly inaccessible cardinal 強到達不能基数
Σ1_1 induction Σ1_1 帰納法
higher-order universe 高階宇宙
recursion 再帰
large hierarchy 大きな階層
reflection principle 反射原理
conservativity result 保守性結果
induction scheme 帰納法スキーム
logic translation 論理翻訳
constructive mathematics 構成的数学
untyped lambda calculus 型無しラムダ計算
recursive function 再帰関数
category theory 圏論
formalisation 形式化
syntactic proof 構文論的証明
semantic version 意味論的バージョン
Π_2-formula Π_2 公式
transfinite hierarchy 超限階層
weakening 弱化
comprehension principle 内包原理
conservation theorem 保存定理、(保存則)
logical consequence 論理的帰結
extensionality 外延性
formalisation of universes 宇宙の形式化
参考
メモ